structure VCreduce = 
struct
  structure V = VC
  structure A = Assert
  structure E = Env
  structure F = Frame
  structure Err = ErrorMsg

  (*=====================basic type====================*)
  type binop = V.binop
  type mytype = V.mytype
  type id = V.id

  datatype exp
    = Expvoid
    | IntNum of int
    | True
    | False
    | Null
    | Lval of lval
    | BinopExp of exp * binop * exp 
    | Not of exp  

    | Imply of exp * exp 
    (*| Iff of exp * exp * pos*) (* e1<=>e2 should be desugared to: e1=>e2 /\ e2=>e1 *)
    | Forall of id * mytype * exp  (* forall exp-- forall x:T.P*)
    | Exists of id * mytype * exp  (* exitst*)
    | Pi of lval list list  (*No Null No Dangling Pointer set *)
    | N of lval list (* Null pointer set*)
    | D of lval list  (* Dangling pointer set *)
    | Prev of lval (* previous value *)
  and lval
    = Var of id
    | Ptr of lval * lval    (*{ Sharp(T, lval) *)
    | Sharp of mytype              (*{ *)
    | Inarray of lval * exp
    | Instruct of lval * id
    | Upd of lval * exp list  * exp
    | Sel of lval * exp
  
  (*====================reduce VC in source level=======*)
  fun reduce vc = 
      let fun hd_exp V.Expvoid = Expvoid
	    | hd_exp (V.IntNum(i)) = IntNum(i)
	    | hd_exp V.True = True
	    | hd_exp V.False = False
	    | hd_exp V.Null = Null
	    | hd_exp (V.Lval(l)) = Lval(reduce' l)
	    | hd_exp (V.BinopExp(e1, bop, e2)) = 
	      BinopExp(hd_exp e1, bop, hd_exp e2)
	    | hd_exp (V.Not(e)) = Not(hd_exp e)
	    | hd_exp (V.Imply(e1, e2)) = 
	      Imply(hd_exp e1, hd_exp e2)
	    | hd_exp (V.Forall(id, tp, e)) = 
	      Forall(id, tp, hd_exp e)
	    | hd_exp (V.Exists(id, tp, e)) = 
	      Exists(id, tp, hd_exp e)
	    | hd_exp (V.Pi(l)) = raise Fail "not yet\n"
	    | hd_exp (V.N(l)) = raise Fail "not yet\n"
	    | hd_exp (V.D(l)) = raise Fail "not yet\n"
	    | hd_exp (V.Prev(l)) = raise Fail "not yet\n"
	    | hd_exp _ = raise Fail "not yet\n"
      in hd_exp vc
      end
  and reduce' lval = 
      let fun hd_lv (V.Var(id)) = Var(id)
	    | hd_lv (V.Sel(lv, e)) = Sel(reduce' lv, reduce e)
	    | hd_lv (V.Upd(lv, e1, V.Lval(V.Upd(lv', e2, e3)))) = 
	      if V.Sel(lv, e1) = lv'
	      then Upd(reduce' lv, (reduce e1)::[reduce e2], reduce e3)
	      else Upd(reduce' lv, [reduce e1], Lval(Upd(reduce' lv', [reduce e2],reduce e3)))
	    | hd_lv (V.Upd(lv, e1, e2)) = 
	      Upd(reduce' lv, [reduce e1], reduce e2)
	    | hd_lv (V.Sharp(tp)) = Sharp(tp)
	    | hd_lv _ = raise Fail "bug\n"
      in hd_lv lval
      end

  fun red_top svclist = 
      let val cl_vc = List.map Irvc2vc.newmap svclist
      in  List.map (fn (id, prop) => (id, reduce prop)) cl_vc
      end
  
  (*=============translate to VC in low level=========*)
  fun mapToAddr (id) = 0 (* cheat compiler! *)
  (* translation based on cleaned_IR, NOT AST!*)
  fun transLval' lval infunc env senv (st:A.state) = 
      let fun trans (Var(id)) = 
	      let val aaa = E.lookup id env
		  val (islocal, offset,types) = 
		      case aaa
		       of SOME(v) => v
			| NONE => raise Fail "no this case, compiler bug\n"
	      in if islocal 
                    then let val roff = if infunc 
					then A.Plus(A.Sel(#1 st, A.Ebp), A.IntNum(offset))
					else A.Plus(A.Sel(#1 st, A.Esp), A.IntNum(offset+8))
			 in  (fn E.Simple => (A.Sel(#2 st, roff), types, st)
			       | (E.Pointer(tp')) => (A.Sel(#2 st, roff), types, st)
			       | _ => (roff, types, st)) types
			 end
                  else (fn E.Simple => (A.Sel(#2 st, A.Addr(mapToAddr(id))), types, st)
			 | (E.Pointer(tp')) => (A.Sel(#2 st, A.Addr(mapToAddr(id))), types, st)
			 | _ => (A.Addr(mapToAddr(id)), types, st)) types
              end
	    | trans (Sel(lval, exp)) = 
	      let val (subexp, types, st') = transLval' lval infunc env senv st
	      in (fn (E.Pointer(subtype)) => 
		     let val subexp' = transExp' exp infunc env senv st
		     in (fn E.Simple => (A.Sel(#2 st', subexp'), subtype, st')
			  | (E.Pointer(tp')) => (A.Sel(#2 st', subexp'), subtype, st')
			  | _ => (subexp', subtype, st')) subtype
		     end
		   | (E.Array(_,subtype)) => 
		     let val elemSize = E.calTypeSize subtype senv
			 val index = transExp' exp infunc env senv st
			 val offset = A.Times(index, A.IntNum(elemSize))
		     in  (fn E.Simple => (A.Sel(#2 st', A.Plus(subexp, offset)), subtype, st')
			   | (E.Pointer(tp')) => (A.Sel(#2 st', A.Plus(subexp, offset)), subtype, st')
			   | _ => (A.Plus(subexp, offset), subtype, st')) subtype
		     end
		   | (E.Struct(str)) => 
		     let val id = (fn (Lval(Var(s))) => s
				    | _ => raise Fail "bug") exp
			 val (offset, rettype) = Option.valOf(E.lookupF str id senv)
		     in (fn E.Simple => (A.Sel(#2 st', A.Plus(subexp, A.IntNum(offset))), rettype, st')
			  | (E.Pointer(tp')) => (A.Sel(#2 st', A.Plus(subexp, A.IntNum(offset))), rettype, st')
			  | _ => (A.Plus(subexp, A.IntNum(offset)), rettype, st')) rettype
		     end
		   | E.Simple => raise Fail "bug") types
	      end
	    | trans (Sharp(tp)) = 
	      let fun cvtType (VC.Int) = E.Simple 
		    | cvtType (VC.Bool) = E.Simple
		    | cvtType (VC.Void) = E.Simple
		    | cvtType (VC.Struct(id)) = E.Struct(id)
		    | cvtType (VC.Pointer(subtype)) = E.Pointer(cvtType(subtype))
		    | cvtType (VC.Array(i, subtype)) = E.Array(i, cvtType(subtype))
		  val newtp = cvtType tp
	      in (A.IntNum(1),E.Pointer(newtp), st) 
	      end
	    | trans (Upd(lv, sel_seq, e2)) = 
	      let fun fd lv0 (e::r) = fd (Sel(lv0, e)) r
		    | fd lv0 [] = lv0
		  val lv' = fd lv sel_seq
		  val (modexp', dummy_tp, st') = transLval' lv' infunc env senv st
		  val modexp = (fn (A.Sel(_, ad)) => ad
				 | ad => ad) modexp'
		  val (subexp, types, dummy_st)  = transLval' lv infunc env senv st
		  val newe = transExp' e2 infunc env senv st'(*WIP*)
		  val newst = (#1 st, A.Upd((#2 st'), modexp, newe))
	      in (*(subexp, types, newst)*)
		  (subexp, types, newst)
	      end
	    | trans _ = raise Fail "should not happen!"
      in trans lval
      end
  
  and transExp' exp infunc env senv (st:A.state) = 
      let fun trans (IntNum(i)) = A.IntNum(i)
            | trans (Null) = A.Addr(0)
            | trans (BinopExp(e1, binop, e2)) =
              let val e1' = (transExp' e1 infunc env senv st)
                  val e2' = (transExp' e2 infunc env senv st)
              in  case binop
                   of  VC.Plus => A.Plus(e1', e2')
                     | VC.Minus => A.Minus(e1', e2')
                     | VC.Times => A.Times(e1', e2')
                     | _ => (raise Fail "impossible"; A.Minus(e1', e2'))
              end
            | trans (Lval(lval)) = #1 (transLval' lval infunc env senv st)
            | trans _ = (raise Fail "impossible"; A.IntNum(0))
      in  trans exp
      end 

  fun transProp' exp infunc env senv st = 
      let fun trans True = A.True
	    | trans False = A.Not(A.True)
	    | trans (BinopExp(e1,binop, e2)) =
	      (case binop
                of  VC.Band => 
                    A.And(transProp' e1 infunc env senv st, transProp' e2 infunc env senv st)
                  | VC.Bor =>
                    A.Or(transProp' e1 infunc env senv st, transProp' e2 infunc env senv st)
                  | VC.GT =>
                    A.Gt(transExp' e1 infunc env senv st, transExp' e2 infunc env senv st)
                  | VC.GE =>
                    A.Ge(transExp' e1 infunc env senv st, transExp' e2 infunc env senv st)
                  | VC.LT =>
                    A.Lt(transExp' e1 infunc env senv st, transExp' e2 infunc env senv st)
                  | VC.LE =>
                    A.Le(transExp' e1 infunc env senv st, transExp' e2 infunc env senv st)
                  | VC.Equ =>
                    A.Eq(transExp' e1 infunc env senv st, transExp' e2 infunc env senv st)
                  | VC.NEqu =>
                    A.Ne(transExp' e1 infunc env senv st, transExp' e2 infunc env senv st)
                  | _ => (raise Fail "impossible"; A.True))
	    | trans (Not(e)) = A.Not(transProp' e infunc env senv st)
	    | trans (Imply(e1, e2)) = 
              A.Imply(transProp' e1 infunc env senv st, transProp' e2 infunc env senv st)
	    | trans (Forall(id, tp, e)) = 
	      trans e
	    | trans _ = (raise Fail "not yet";A.True)
      in trans exp
      end 
  
    (* for each function *)
  fun tr_fun (fname, rettype, alist, llist) (env, senv) svclist = 
      let val frame = F.newFrame fname rettype
          val env1 = Codegen.buildEnv alist env senv frame F.allocArgs
          val newenv = Codegen.buildEnv llist env1 senv frame F.allocLocals
	  fun findvc ((fid, s)::r) = if fid = fname
				     then s
				     else findvc r
	    | findvc [] = True
	  val svc = findvc svclist
	  val avc = transProp' svc false newenv senv 
      in (fname, avc)
      end
  
  (* emit low-level vc*)
  fun emitVC ast svclist = 
      let val coqfile = TextIO.openOut((!Err.fileName)^"4.v")
	  val genv = Svc2avc.bd_env ast
	  val red_vc = red_top svclist
	  fun trans (Ast.ExdecFunc(id, rettype, arg, var, stm, pre, post, pos)) = 
	      [tr_fun (id, rettype, arg, var) genv red_vc]
	    | trans (Ast.ExdecSeq(s1, s2, pos)) = (trans s1)@(trans s2)
	    | trans _ = []
	  val avclist = trans ast
	  val coqtext = String.concat(List.map LCoqize.asst2coq avclist)
      in  TextIO.output(coqfile, coqtext);
          TextIO.closeOut(coqfile)
      end
end